|
In theoretical computer science, in particular in term rewriting, a path ordering is a well-founded strict total order (>) on the set of all terms such that :''f''(...) > ''g''(''s''1,...,''s''''n'') if ''f'' .> ''g'' and ''f''(...) > ''s''''i'' for ''i''=1,...,''n'', where (.>) is a user-given total precedence order on the set of all function symbols. Intuitively, a term ''f''(...) is bigger than any term ''g''(...) built from terms ''s''''i'' smaller than ''f''(...) using a lower-precedence root symbol ''g''. In particular, by structural induction, a term ''f''(...) is bigger than any term containing only symbols smaller than ''f''. A path ordering is often used as reduction ordering in term rewriting, in particular in the Knuth–Bendix completion algorithm. As an example, a term rewriting system for "multiplying out" mathematical expressions could contain a rule ''x'' *(''y''+''z'') → (''x'' *''y'') + (''x'' *''z''). In order to prove termination, a reduction ordering (>) must be found with respect to which the term ''x'' *(''y''+''z'') is greater than the term (''x'' *''y'')+(''x'' *''z''). This is not trivial, since the former term contains both less function symbols and less variables than the latter. However, setting the precedence ( *) .> (+), a path ordering can be used, since both ''x'' *(''y''+''z'') > ''x'' *''y'' and ''x'' *(''y''+''z'') > ''x'' *''z'' is easy to achieve. Given two terms ''s'' and ''t'', with a root symbol ''f'' and ''g'', respectively, to decide their relation their root symbols are compared first. * If ''f'' <. ''g'', then ''s'' can dominate ''t'' only if one of ''ss subterms does. * If ''f'' .> ''g'', then ''s'' dominates ''t'' if ''s'' dominates each of ''ts subterms. * If ''f'' = ''g'', then the immediate subterms of ''s'' and ''t'' need to be compared recursively. Depending on the particular method, different variations of path orderings exist.〔 Here: sect.5.3, p.275〕〔 Here: chapter 4, p.55-64〕 The latter variations include: * the multiset path ordering (mpo), originally called recursive path ordering (rpo) * the lexicographic path ordering (lpo) * a combination of mpo and lpo, called recursive path ordering by Dershowitz, Jouannaud (1990)〔Kamin, Levy (1980)〕 Dershowitz, Okada (1988) list more variants, and relate them to Ackermann's system of ordinals. ==Formal definitions== The multiset path ordering (>) can be defined as follows:〔Huet (1986), sect.4.3, def.1, p.57〕 , | or |- | ''f'' | = | ''g'' | and | colspan=5 | >> |} where * (≥) denotes the reflexive closure of the mpo (>), * denotes the multiset of ''s''’s subterms, similar for ''t'', and * (>>) denotes the multiset extension of (>), defined by >> if can be obtained from * * by deleting at least one element, or * * by replacing an element by a multiset of strictly smaller (w.r.t. the mpo) elements.〔Huet (1986), sect.4.1.3, p.56〕 More generally, an order functional is a function ''O'' mapping an ordering to another one, and satisfying the following properties:〔Huet (1986), sect.4.3, p. 58〕 * If (>) is transitive, then so is ''O''(>). * If (>) is irreflexive, then so is ''O''(>). * If ''s'' > ''t'', then ''f''(...,''s'',...) ''O''(>) ''f''(...,''t'',...). * ''O'' is continuous on relations, i.e. if ''R''0, ''R''1, ''R''2, ''R''3, ... is an infinite sequence of relations, then ''O''(∪ ''R''''i'') = ∪ ''O''(''R''''i''). The multiset extension, mapping (>) above to (>>) above is one example of an order functional: (>>)=''O''(>). Another order functional is the lexicographic extension, leading to the lexicographic path ordering. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Path ordering (term rewriting)」の詳細全文を読む スポンサード リンク
|